$\forall$${\it es}$:ES, $S$:E List. es{-}seq(${\it es}$;$S$) $\in$ Prop